Fix #1198: [Rule] IntegerExpressionMembership to binary ILP - #1243

#!/usr/bin/env python3
"""Seven-section finite audit. Run with python3 (sympy and hypothesis required).

Expression: positive int, or ('u'|'+', left, right). Rows: (sorted (index,coeff), rhs).
The exact binary CSP solver knows only emitted rows, not expressions or carries.
Checks are counted assertions, never claimed as independent random samples.
"""
from collections import Counter, deque
from dataclasses import dataclass
from functools import lru_cache
from itertools import product
import json
from pathlib import Path
import random
import subprocess
import sys

import sympy as sp
from hypothesis import given, seed, settings, strategies as st

MAX_I64 = (1 << 63) - 1
MAX_USIZE = (1 << 64) - 1
SEED = 2026110401
COUNTS = Counter()
STATS = Counter()
ROOT = Path(__file__).resolve().parents[1]


def check(section, condition, context):
    COUNTS[section] += 1
    if not condition:
        raise AssertionError(f"section {section}: {context}")


def checked(value, maximum=MAX_USIZE):
    if not 0 <= value <= maximum:
        raise OverflowError("layout count outside usize")
    return value


def layout(a, s, u, h, maximum=MAX_USIZE):
    if a < 1 or s < 0 or u < 0 or s + u != a - 1 or not 1 <= h <= 63:
        raise ValueError("invalid tree counts or width")
    # Subtract before doubling so an intermediate cannot reject a fitting T.
    t = checked(a + checked(a - 1, maximum), maximum)
    p = checked(a * h, maximum)
    c = checked(a * (h - 1), maximum)
    n = checked(checked(t + p, maximum) + c, maximum)
    m = checked(checked(checked(checked(1 + 2 * s, maximum) + u, maximum) + p, maximum) + h, maximum)
    return t, n, m


@dataclass(frozen=True)
class Target:
    nodes: tuple
    h: int
    n: int
    rows: tuple
    bounds: tuple
    objective: tuple = ()
    sense: str = "Minimize"

    def feasible(self, witness):
        if len(witness) != self.n:
            raise ValueError("wrong target witness length")
        if any(type(x) is not int or not lo <= x <= hi
               for x, (lo, hi) in zip(witness, self.bounds)):
            return False
        return all(sum(c * witness[i] for i, c in terms) == rhs
                   for terms, rhs in self.rows)

    def extract(self, witness):
        if not self.feasible(witness):
            raise ValueError("infeasible target witness")
        choices = []

        def walk(t):
            kind, left, right = self.nodes[t]
            if kind == '+':
                walk(left)
                walk(right)
            elif kind == 'u':
                choice = witness[right] == 1
                choices.append(choice)
                walk(right if choice else left)
        walk(0)
        u = sum(kind == 'u' for kind, _, _ in self.nodes)
        return tuple(choices) + (False,) * (u - len(choices))

    def solutions(self):
        """Complete finite-domain search with exact per-row support propagation.

        Each row's truth table is computed from the target itself. Every pruning
        removes only values lacking support in that row; branching exhausts both
        remaining values. Thus this enumerates all solutions, including spurious
        solutions of a faulty construction. No source/lift routine is consulted.
        """
        tables = []
        incident = [[] for _ in range(self.n)]
        for rid, (terms, rhs) in enumerate(self.rows):
            indices = tuple(i for i, _ in terms)
            allowed = tuple(tuple(1 << bit for bit in bits)
                            for bits in product((0, 1), repeat=len(terms))
                            if sum(c * b for (_, c), b in zip(terms, bits)) == rhs)
            tables.append((indices, allowed))
            for i in indices:
                incident[i].append(rid)

        def search(domains, pending):
            queue = deque(pending)
            queued = set(pending)
            while queue:
                rid = queue.popleft()
                queued.remove(rid)
                indices, table = tables[rid]
                supports = [0] * len(indices)
                for row in table:
                    if all(domains[i] & v for i, v in zip(indices, row)):
                        for k, v in enumerate(row):
                            supports[k] |= v
                if not table or any(not x for x in supports):
                    return
                for i, support in zip(indices, supports):
                    narrowed = domains[i] & support
                    if not narrowed:
                        return
                    if narrowed != domains[i]:
                        domains[i] = narrowed
                        for other in incident[i]:
                            if other not in queued:
                                queued.add(other)
                                queue.append(other)
            index = next((i for i, d in enumerate(domains) if d == 3), None)
            if index is None:
                witness = tuple(d - 1 for d in domains)
                if self.feasible(witness):
                    yield witness
                return
            for bit in (1, 2):
                branch = domains.copy()
                branch[index] = bit
                yield from search(branch, incident[index])
        yield from search([3] * self.n, range(len(self.rows)))


def reduce(expression, target):
    if type(target) is not int or not 1 <= target <= MAX_I64:
        raise ValueError("target outside positive i64")
    nodes = []
    atoms = []

    def flatten(e):
        t = len(nodes)
        nodes.append(None)
        if type(e) is int:
            if not 1 <= e <= MAX_I64:
                raise ValueError("atom outside positive i64")
            nodes[t] = ('a', e, None)
            atoms.append((t, e))
        else:
            kind, l, r = e
            if kind not in ('+', 'u'):
                raise ValueError("unknown operator")
            left, right = flatten(l), flatten(r)
            nodes[t] = (kind, left, right)
        return t
    flatten(expression)
    a = len(atoms)
    s = sum(kind == '+' for kind, _, _ in nodes)
    u = sum(kind == 'u' for kind, _, _ in nodes)
    h = max(target.bit_length(), *(v.bit_length() for _, v in atoms))
    t, n, m = layout(a, s, u, h)
    rows = []

    def row(terms, rhs=0):
        # Match the real model's sparse normalization.
        coefficients = Counter()
        for i, c in terms:
            coefficients[i] += c
        rows.append((tuple(sorted((i, c) for i, c in coefficients.items() if c)), rhs))

    def p(j, b):
        return t + j * h + b

    def c(j, b):
        return t + a * h + j * (h - 1) + b - 1

    row([(0, 1)], 1)
    for i, (kind, l, r) in enumerate(nodes):
        if kind == '+':
            row([(l, 1), (i, -1)])
            row([(r, 1), (i, -1)])
        elif kind == 'u':
            row([(l, 1), (r, 1), (i, -1)])
    for j, (leaf, value) in enumerate(atoms):
        for b in range(h):
            terms = [(p(j, b), -1)]
            if j:
                terms.append((p(j - 1, b), 1))
            if (value >> b) & 1:
                terms.append((leaf, 1))
            if b:
                terms.append((c(j, b), 1))
            if b + 1 < h:
                terms.append((c(j, b + 1), -2))
            row(terms)
    for b in range(h):
        row([(p(a - 1, b), 1)], (target >> b) & 1)
    if len(rows) != m:
        raise AssertionError("row allocation disagrees with layout")
    return Target(tuple(nodes), h, n, tuple(rows), ((0, 1),) * n)


def source_counts(e):
    if type(e) is int:
        return 1, 0, 0, 1, e.bit_count()
    a, s, u, t, b = source_counts(e[1])
    aa, ss, uu, tt, bb = source_counts(e[2])
    return a + aa, s + ss + (e[0] == '+'), u + uu + (e[0] == 'u'), t + tt + 1, b + bb


def reachable(e):
    """Independent denotational oracle: form union/Minkowski sum sets."""
    if type(e) is int:
        return {e}
    left, right = reachable(e[1]), reachable(e[2])
    if e[0] == 'u':
        return left | right
    return {x + y for x in left for y in right if x + y <= MAX_I64}


def evaluate_source(e, witness):
    if len(witness) != source_counts(e)[2] or any(type(x) is not bool for x in witness):
        raise ValueError("wrong source encoding")
    it = iter(witness)

    def visit(node):
        if type(node) is int:
            return node
        if node[0] == 'u':
            return visit(node[2] if next(it) else node[1])
        left = visit(node[1])
        if left is None:
            return None
        right = visit(node[2])
        if right is None or left + right > MAX_I64:
            return None
        return left + right
    return visit(e)


def lift(e, witness, target):
    """Forward extension by visited source choices and ordinary bit addition.

    On an overflowing addition, discard the terminal carry; target rows must
    then reject this candidate. This is deliberate negative evidence.
    """
    choices = iter(witness)
    active = [0] * len(target.nodes)

    def walk(t):
        active[t] = 1
        kind, l, r = target.nodes[t]
        if kind == '+':
            walk(l)
            walk(r)
        elif kind == 'u':
            walk(r if next(choices) else l)
    walk(0)
    prefixes, carries = [], []
    previous = [0] * target.h
    for t, (kind, value, _) in enumerate(target.nodes):
        if kind != 'a':
            continue
        bits, carry = [], 0
        for b in range(target.h):
            total = previous[b] + ((value >> b) & 1) * active[t] + carry
            bits.append(total % 2)
            carry = total // 2
            if b + 1 < target.h:
                carries.append(carry)
        prefixes.extend(bits)
        previous = bits
    return tuple(active + prefixes + carries)


def measured(t):
    magnitudes = [1] + [abs(x) for terms, rhs in t.rows for x in [rhs, *(c for _, c in terms)]]
    return t.n, len(t.rows), sum(len(terms) for terms, _ in t.rows), max(magnitudes).bit_length()


def audit(e, k, family):
    target = reduce(e, k)
    STATS['instances'] += 1
    STATS[family] += 1
    solutions = tuple(target.solutions())
    values = reachable(e)
    a, s, u, t, b = source_counts(e)
    source_values = set()
    for config in product((False, True), repeat=u):
        value = evaluate_source(e, config)
        if value is not None:
            source_values.add(value)
        candidate = lift(e, config, target)
        check(2, target.feasible(candidate) == (value == k), (family, e, k, config, 'forward'))
    check(2, source_values == values and bool(solutions) == (k in values), (family, e, k, 'equivalence'))
    STATS['feasible targets'] += len(solutions)
    activations = set()
    for witness in solutions:
        config = target.extract(witness)
        check(3, evaluate_source(e, config) == k, (family, e, k, 'extraction'))
        # Unused coordinates form a canonical false tail after the consumed bits.
        used = []
        def visited(i):
            kind, left, right = target.nodes[i]
            if kind == '+':
                visited(left)
                visited(right)
            elif kind == 'u':
                used.append(witness[right] == 1)
                visited(right if witness[right] else left)
        visited(0)
        check(3, config == tuple(used) + (False,) * (u - len(used)), (e, 'unused tail'))
        activation = witness[:t]
        check(5, activation not in activations, (e, k, 'unique arithmetic extension'))
        activations.add(activation)
        # Every single-coordinate mutation of a feasible witness is infeasible:
        # one activation alone violates its tree row; arithmetic is unique.
        for i in range(target.n):
            bad = witness[:i] + (1 - witness[i],) + witness[i + 1:]
            check(3, not target.feasible(bad), (e, k, i, 'single bit corruption'))
        for bad in (witness[:-1], witness + (0,), (2,) + witness[1:]):
            rejected = False
            try:
                target.extract(bad)
            except ValueError:
                rejected = True
            check(3, rejected, 'extract rejects bad length or nonbinary witness')
        # Actual target pins must reject the opposite query, independent of encoding.
        wrong_query = reduce(e, k + 1) if k < MAX_I64 else reduce(e, k - 1)
        if wrong_query.n == target.n:
            check(2, not wrong_query.feasible(witness), 'final query pins are effective')
    h = target.h
    expected = (t + a * (2 * h - 1), 1 + 2 * s + u + a * h + h,
                a * (4 * h - 2) + b + 1 + 4 * s + 3 * u, 1 if h == 1 else 2)
    check(4, measured(target) == expected, (family, e, k, measured(target), expected))
    well_formed = (target.bounds == ((0, 1),) * target.n and target.objective == () and target.sense == 'Minimize')
    for terms, rhs in target.rows:
        ids = [i for i, _ in terms]
        well_formed &= (bool(terms) and ids == sorted(set(ids)) and all(0 <= i < target.n for i in ids)
                        and rhs in (0, 1) and all(c in (-2, -1, 1) for _, c in terms)
                        and sum(max(c, 0) for _, c in terms) <= 3
                        and sum(min(c, 0) for _, c in terms) >= -3)
    check(5, well_formed, (e, k, 'target domains, normalization and row arithmetic'))
    if target.n <= 12:
        raw = {x for x in product((0, 1), repeat=target.n) if target.feasible(x)}
        check(5, raw == set(solutions), (e, k, 'complete raw-domain solver calibration'))
        STATS['raw-domain assignments'] += 1 << target.n
    return target, solutions


def symbolic():
    a, s, u, t, h, b = sp.symbols('A S U T H B', integer=True, positive=True)
    identities = [
        (t + a * h + a * (h - 1), t + a * (2 * h - 1)),
        (1 + 2 * s + u + a * h + h, 1 + 2 * s + u + h * (a + 1)),
        (1 + 4 * s + 3 * u + h * (a - 1) + b + 2 * a * (h - 1) + a * h + h,
         a * (4 * h - 2) + b + 1 + 4 * s + 3 * u),
    ]
    example = reduce(('+', 1, 2), 3)
    observed = measured(example)
    for metric, (blocks, formula) in enumerate(identities):
        instantiated = formula.subs({a: 2, s: 1, u: 0, t: 3, h: 2, b: 2})
        check(1, sp.simplify(blocks - formula) == 0 and observed[metric] == instantiated,
              ('symbolic overhead tied to constructed target', metric))
    # Exact magnitude branch is bounded by 2, including the no-carry branch.
    for width in range(1, 64):
        target = reduce(1 << (width - 1), 1 << (width - 1))
        bound = sp.Integer(1 if width == 1 else 2)
        check(1, bool(bound <= 2) and measured(target)[3] == bound, ('magnitude', width))
        # Formal coefficients of carries in the weighted row sum cancel.
        carries = sp.symbols(f'c0:{width + 1}')
        weighted = sum(2 ** bit * (carries[bit] - 2 * carries[bit + 1]) for bit in range(width))
        identity = carries[0] - 2 ** width * carries[-1]
        check(1, sp.expand(weighted - identity) == 0 and target.feasible((1,) + (0,) * (width - 1) + (1,) + (0,) * (width - 1)),
              ('telescoping and emitted atom rows', width))


@lru_cache(None)
def trees(nodes):
    if nodes == 1:
        return (1, 2, 3)
    return tuple((op, left, right)
                 for left_size in range(1, nodes - 1, 2)
                 for left in trees(left_size)
                 for right in trees(nodes - 1 - left_size)
                 for op in ('u', '+'))


def random_tree(u, s, rng):
    if u + s == 0:
        return rng.randint(1, 31)
    op = rng.choice(['u'] * u + ['+'] * s)
    u, s = u - (op == 'u'), s - (op == '+')
    lu, ls = rng.randint(0, u), rng.randint(0, s)
    return op, random_tree(lu, ls, rng), random_tree(u - lu, s - ls, rng)


def boundary_checks():
    for e, k in [(1, 1), (1, 2), (('+', 1, 1), 1), (('u', 1, 1), 1),
                 (('+', 1, 2), 3), (('u', 1, 2), 8), (MAX_I64, MAX_I64),
                 (('+', MAX_I64 - 1, 1), MAX_I64), (('+', MAX_I64, 1), MAX_I64),
                 (('u', ('+', MAX_I64, 1), 3), 3),
                 (('+', ('u', ('u', 1, 2), 3), ('u', 4, 5)), 8)]:
        target, solutions = audit(e, k, 'special')
        if e == ('+', MAX_I64 - 1, 1):
            carry_start = len(target.nodes) + 2 * target.h
            check(5, len(solutions) == 1 and solutions[0][carry_start:] == (0,) * 124,
                  'all-ones maximum result has no carries')
        if k == 8 and type(e) is tuple and e[0] == '+':
            check(3, {target.extract(w) for w in solutions} == {(True, True, False)}, 'visited DFS regression')
    for width in range(1, 64):
        power = 1 << (width - 1)
        audit(('u', power, min(MAX_I64, power + 1)), power, 'bit boundaries')
        if power > 1:
            target, solutions = audit(('+', power - 1, 1), power, 'bit boundaries')
            if width == 63:
                carry_start = len(target.nodes) + 2 * target.h
                check(5, len(solutions) == 1 and solutions[0][carry_start:] == (0,) * 62 + (1,) * 62,
                      'width-63 power-of-two result has 62 consecutive carries')
    for atom, query in [(0, 1), (-1, 1), (MAX_I64 + 1, 1), (1, 0), (1, -1), (1, MAX_I64 + 1)]:
        rejected = False
        try:
            reduce(atom, query)
        except ValueError:
            rejected = True
        # Tie each rejection to a real constructed target as well as the input boundary.
        check(2, rejected and reduce(1, 1).feasible((1, 1)), ('input boundary', atom, query))
    reference = reduce(1, 1)
    for maximum in (255, MAX_USIZE):
        for h in (1, 63):
            for only_sums in (False, True):
                # Independent closed forms for legal full trees.
                n_limit = (maximum + 1) // (2 * h + 1)
                m_limit = ((maximum - h + 1) // (h + 2) if only_sums
                           else (maximum - h) // (h + 1))
                last = min(n_limit, m_limit)
                s, u = (last - 1, 0) if only_sums else (0, last - 1)
                result = layout(last, s, u, h, maximum)
                rejected = False
                try:
                    layout(last + 1, s + only_sums, u + (not only_sums), h, maximum)
                except OverflowError:
                    rejected = True
                check(2, max(result) <= maximum and rejected and reference.feasible((1, 1)),
                      ('layout last accepted / first rejected', maximum, h, only_sums))
    for h in (0, 64):
        rejected = False
        try:
            layout(1, 0, 0, h)
        except ValueError:
            rejected = True
        check(2, rejected and reference.h == 1 and reference.n == 2, ('width neighbour', h))


def hypothesis_cases():
    small = st.recursive(st.integers(1, 7),
                         lambda children: st.tuples(st.sampled_from(('u', '+')), children, children),
                         max_leaves=6)
    extreme = st.one_of(st.integers(1, 31), st.sampled_from(((1 << 62) - 1, 1 << 62, MAX_I64 - 1, MAX_I64)))

    @seed(SEED + 1)
    @settings(max_examples=300, database=None, deadline=None)
    @given(small, st.integers(1, 50))
    def general(e, k):
        audit(e, k, 'hypothesis recursive')

    @seed(SEED + 2)
    @settings(max_examples=300, database=None, deadline=None)
    @given(extreme, extreme, st.booleans())
    def signed_edges(x, y, right):
        # Inactive overflow alternatives combined with a later consumed union bit.
        e = ('+', ('u', ('+', x, MAX_I64), 1), ('u', y, 2))
        k = 3 if right else min(MAX_I64, 1 + y)
        audit(e, k, 'hypothesis signed')
    general()
    signed_edges()


def sensitivity():
    # The following mutants are witnesses/rows, never alternate constructors.
    # Each case checks that a defining restriction prevents a known false result.
    target = reduce(1, 1)
    no_root = Target(target.nodes, target.h, target.n, target.rows[1:], target.bounds)
    check(5, target.feasible((1, 1)) and not no_root.feasible((0, 1)), 'atom still linked without root')
    target = reduce(1, 2)
    removed = Target(target.nodes, target.h, target.n, target.rows[:-target.h], target.bounds)
    check(5, not list(target.solutions()) and bool(list(removed.solutions())), 'final pins essential')
    target = reduce(('u', 1, 2), 3)
    rows = target.rows[:1] + target.rows[2:]
    removed = Target(target.nodes, target.h, target.n, rows, target.bounds)
    check(5, not list(target.solutions()) and bool(list(removed.solutions())), 'union exclusivity essential')
    target = reduce(('+', 1, ('+', 1, 1)), 1)
    # H=1: remove the middle addition equality, allowing its outgoing carry loss.
    arithmetic_start = 1 + 2 * 2
    rows = target.rows[:arithmetic_start + 1] + target.rows[arithmetic_start + 2:]
    removed = Target(target.nodes, target.h, target.n, rows, target.bounds)
    check(5, not list(target.solutions()) and bool(list(removed.solutions())), 'terminal overflow restriction essential')
    target = reduce(('u', 1, 1), 1)
    zero = (0,) * target.n
    # Without root and final rows, all-zero would satisfy every homogeneous row.
    homogeneous = Target(target.nodes, target.h, target.n, target.rows[1:-target.h], target.bounds)
    check(5, not target.feasible(zero) and homogeneous.feasible(zero), 'root/pin homogeneous trap')


def examples():
    e = ('+', ('+', ('u', 1, 4), ('u', 3, 6)), ('u', 2, 5))
    yes, solutions = audit(e, 12, 'worked YES')
    activation = (1,1,1,0,1,1,0,1,1,1,0)
    prefixes = ((0,0,0,0), (0,0,1,0), (0,0,1,0), (0,1,0,1), (0,0,1,1), (0,0,1,1))
    carries = ((0,0,0), (0,0,0), (0,0,0), (0,0,1), (0,1,0), (0,0,0))
    witness = activation + sum(prefixes, ()) + sum(carries, ())
    check(6, measured(yes) == (53, 36, 111, 2) and source_counts(e) == (6, 2, 3, 11, 9), 'YES counts')
    check(6, witness in solutions and yes.feasible(witness) and yes.extract(witness) == (True,True,False), 'YES complete witness')
    for j, total in enumerate((0,4,4,10,12,12)):
        start = 11 + 4 * j
        encoded = sum(yes_weight << b for b, yes_weight in enumerate(witness[start:start + 4]))
        check(6, yes.feasible(witness) and encoded == total, ('YES prefix', j))
    no, solutions = audit(e, 7, 'worked NO')
    check(7, reachable(e) == {6,9,12,15} and not solutions and measured(no) == (41,29,87,2), 'NO numbers and infeasibility')
    for config in product((False, True), repeat=3):
        check(7, evaluate_source(e, config) != 7 and not no.feasible(lift(e, config, no)), ('NO choices', config))


def rust_calibration():
    """Calibrate both Python endpoint checkers against actual current Rust models."""
    pred = ROOT / 'problem-reductions/target/debug/pred'
    def cli(*args, stdin=None):
        return subprocess.run([str(pred), *args], input=stdin, text=True, capture_output=True)
    def serialized(e):
        return {'Atom': e} if type(e) is int else {('Union' if e[0] == 'u' else 'Sum'): [serialized(e[1]), serialized(e[2])]}
    log = []
    cases = [(('+', ('u', ('u', 1, 2), 3), ('u', 4, 5)), 8, (True,True,False)),
             (('u', ('+', MAX_I64, 1), 3), 3, (True,)),
             (('+', MAX_I64, 1), MAX_I64, ()), (1, 1, ())]
    for e, k, config in cases:
        created = cli('create', 'IntegerExpressionMembership', '--expression', json.dumps(serialized(e)), '--target', str(k), '--json')
        if created.returncode:
            raise RuntimeError(f'Rust source creation failed: {created.stderr}')
        evaluated = cli('evaluate', '-', '--config', json.dumps(config), '--json', stdin=created.stdout)
        if evaluated.returncode:
            raise AssertionError(evaluated.stderr)
        data = json.loads(evaluated.stdout)
        log.append({'kind': 'source', 'expression': serialized(e), 'target': k, 'config': config, 'result': data})
        check(2, data['result'] == f'Or({str(evaluate_source(e, config) == k).lower()})', ('Rust source evaluate', data))
    target = reduce(('+', 1, 2), 3)
    rows = [{'terms': terms, 'comparison': 'Eq', 'rhs': rhs} for terms, rhs in target.rows]
    target_json = json.dumps({'type':'ILP',
                              'variant':{'variable':'bool','coefficient':'i64','bounds':'general'},
                              'data':{'variables':[{'lower_bound':0,'upper_bound':1}] * target.n,
                                      'constraints':rows, 'objective':[], 'sense':'Minimize'}})
    good = lift(('+',1,2), (), target)
    for witness in (good, (0,) * target.n, (2,) + good[1:], good[:-1]):
        evaluated = cli('evaluate', '-', '--config', json.dumps(witness), '--json', stdin=target_json)
        log.append({'kind':'target', 'config': witness, 'exit': evaluated.returncode, 'output': evaluated.stdout, 'error':evaluated.stderr})
        if len(witness) != target.n:
            check(5, evaluated.returncode != 0 and target.feasible(good), 'Rust wrong-length evaluation')
        else:
            data = json.loads(evaluated.stdout)
            check(5, evaluated.returncode == 0 and data['result'] == ('Min(0)' if target.feasible(witness) else 'Min(None)'), ('Rust target feasibility', data))
    (ROOT / 'model-calibration.json').write_text(json.dumps(log, indent=2) + '\n')


def main():
    print(f'SEED: {SEED}; Hypothesis seeds {SEED+1}, {SEED+2}; max_examples=300; database=None; deadline=None', flush=True)
    symbolic()
    print('Symbolic identities and width lemmas passed', flush=True)
    rust_calibration()
    for nodes in (1, 3, 5):
        for e in trees(nodes):
            for k in range(1, 11):
                audit(e, k, 'exhaustive')
        print(f'Exhaustive full trees through {nodes} nodes: {STATS["exhaustive"]} instances', flush=True)
    rng = random.Random(SEED)
    for u in range(5):
        for s in range(5):
            for _ in range(300):
                audit(random_tree(u, s, rng), rng.randint(1, 100), 'sampled cells')
        print(f'Sampled U={u}, S=0..4: 300 per cell', flush=True)
    boundary_checks()
    hypothesis_cases()
    sensitivity()
    examples()
    names = {1:'symbolic identities', 2:'forward and backward', 3:'every feasible target extraction',
             4:'measured overhead', 5:'structural invariants and oracle calibration', 6:'worked YES', 7:'worked NO'}
    for i, name in names.items():
        if COUNTS[i] == 0:
            raise AssertionError(f'empty section {i}')
        print(f'SECTION {i} ({name}): {COUNTS[i]} checks, 0 failures')
    print('FAMILIES: ' + json.dumps(dict(sorted(STATS.items()))))
    print(f'TOTAL: {sum(COUNTS.values())} checks, 0 failures')


if __name__ == '__main__':
    try:
        main()
    except Exception:
        import traceback
        traceback.print_exc()
        print(f'TOTAL: {sum(COUNTS.values())} checks, 1 failures')
        sys.exit(1)

#!/usr/bin/env python3
"""Cross-compare `pred reduce` with both verified scripts.

For every shared instance, write the source in IntegerExpressionMembership's
JSON format, run `pred reduce` along the single direct
IntegerExpressionMembership -> ILP/bool/i64 path, and compare the bundle's
target with the targets built by constructor.py and by
adv_reduction.py. proof.typ fixes the coordinate and
row order; the only allowed isomorphism is a permutation of the sparse terms
inside a row, so terms are sorted before comparing and rows are compared in
order. On a subset, `pred solve` of the bundle is checked too: its status must
match the scripts' feasibility and its source solution must satisfy the source.

Exits non-zero on any mismatch or any pred failure.

Usage: python3 cross_compare.py --pred PATH [--quick] [--keep DIR]
"""
from __future__ import annotations

import argparse
import itertools
import json
import os
import random
import shutil
import subprocess
import sys
import tempfile

HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, HERE)
sys.path.insert(0, os.path.join(HERE, "adversary"))

import constructor as C  # noqa: E402
import adv_reduction as R  # noqa: E402

SOURCE = "IntegerExpressionMembership"
TARGET = "ILP/bool/i64"
TARGET_VARIANT = {"variable": "bool", "coefficient": "i64", "bounds": "general"}
SEED = 2026110421
M = R.I64_MAX


# ------------------------------------------------------------ shared instances
def mine_to_c(e):
    if e[0] == "A":
        return e[1]
    return ("u" if e[0] == "U" else "+", mine_to_c(e[1]), mine_to_c(e[2]))


def shared_instances(quick=False):
    A, U, S = R.atom, R.union, R.ssum
    out = []
    yes = S(S(U(A(1), A(4)), U(A(3), A(6))), U(A(2), A(5)))
    out += [("worked-yes", yes, 12), ("worked-no", yes, 7),
            ("nested-skip", S(U(U(A(1), A(2)), A(3)), U(A(4), A(5))), 8),
            ("K-above-reachable", U(A(1), A(2)), 8),
            ("single-atom", A(5), 5), ("single-atom-no", A(5), 4),
            ("H1-sum", S(A(1), A(1)), 1), ("H1-union", U(A(1), A(1)), 1),
            ("H63-atom", A(M), M), ("H63-sum", S(A(M - 1), A(1)), M),
            ("H63-overflow-sum", S(A(M), A(1)), M),
            ("H63-inactive-overflow", U(S(A(M), A(1)), A(M)), M),
            ("H63-carry-chain", S(S(A((1 << 62) - 1), A(1)), A((1 << 62) - 1)), M),
            ("H62-boundary", U(A((1 << 61)), A((1 << 62) - 1)), (1 << 61))]
    # every full binary tree with at most 5 nodes, atoms 1..3, K 1..10
    # (the constructor's exhaustive family)
    trees = []
    for ct in itertools.chain(C.trees(1), C.trees(3), C.trees(5)):
        trees.append(ct)
    rng = random.Random(SEED)
    if quick:
        trees = rng.sample(trees, 40)
    for ct in trees:
        for K in range(1, 11):
            out.append(("exhaustive", ct, K))
    # seeded random larger trees, mixed small and boundary atoms
    for i in range(30 if quick else 200):
        n_leaves = rng.randint(1, 7)

        def build(n):
            if n == 1:
                return A(rng.choice([rng.randint(1, 9), rng.randint(1, M), M, (1 << 62), (1 << 62) - 1]))
            k = rng.randint(1, n - 1)
            return (rng.choice("US"), build(k), build(n - k))

        e = build(n_leaves)
        reach = sorted(v for v in R.reachable(e) if v <= M)
        K = rng.choice(reach) if reach and rng.random() < 0.6 else rng.randint(1, M)
        out.append(("random", e, K))
    norm = []
    for fam, e, K in out:
        if not isinstance(e, tuple) or e[0] not in ("A", "U", "S"):
            e = c_to_mine(e)
        norm.append((fam, e, K))
    return norm


def c_to_mine(ce):
    if type(ce) is int:
        return ("A", ce)
    return ("U" if ce[0] == "u" else "S", c_to_mine(ce[1]), c_to_mine(ce[2]))


# ------------------------------------------------------------ canonical forms
def canon_pred(data):
    return (tuple((v.get("lower_bound"), v.get("upper_bound")) for v in data["variables"]),
            tuple((r["comparison"], r["rhs"], tuple(sorted((t[0], t[1]) for t in r["terms"])))
                  for r in data["constraints"]),
            tuple(sorted((t[0], t[1]) for t in data["objective"])),
            data["sense"])


def canon_constructor(t):
    return (tuple(t.bounds), tuple(("Eq", rhs, tuple(sorted(terms))) for terms, rhs in t.rows),
            tuple(sorted(t.objective)), t.sense)


def describe_diff(a, b):
    if a[0] != b[0]:
        return f"variables differ: {len(a[0])} vs {len(b[0])}"
    if len(a[1]) != len(b[1]):
        return f"row count differs: {len(a[1])} vs {len(b[1])}"
    for i, (x, y) in enumerate(zip(a[1], b[1])):
        if x != y:
            same_set = sorted(a[1]) == sorted(b[1])
            return f"row {i} differs: {x} vs {y}" + (" (same rows, different order)" if same_set else "")
    return f"objective/sense differ: {a[2:]} vs {b[2:]}"


# ------------------------------------------------------------ pred plumbing
def run(cmd, timeout=120):
    try:
        r = subprocess.run(cmd, capture_output=True, text=True, timeout=timeout)
    except subprocess.TimeoutExpired:
        return None, f"timeout: {' '.join(cmd)}"
    if r.returncode != 0:
        return None, (r.stderr or r.stdout).strip()
    return r.stdout, None


def find_route(pred, work):
    out, err = run([pred, "path", SOURCE, TARGET, "--limit", "all", "--quiet", "--json"])
    if err:
        return None, f"pred path {SOURCE} {TARGET} failed: {err.splitlines()[0] if err else err}"
    try:
        paths = json.loads(out)["paths"]
    except (ValueError, KeyError) as exc:
        return None, f"pred path output not understood: {exc}"
    direct = [p for p in paths if p.get("steps") == 1]
    if len(direct) != 1:
        return None, f"expected exactly one direct path, found {len(direct)}"
    step = direct[0]["path"]
    # pred path steps are edges: endpoints live in their "from" / "to" objects.
    try:
        ends = (step[0]["from"]["name"], step[-1]["to"]["name"], step[-1]["to"].get("variant"))
    except (KeyError, TypeError, IndexError) as exc:
        return None, f"pred path output not understood: route step lacks {exc}"
    if ends != (SOURCE, "ILP", TARGET_VARIANT):
        return None, f"direct path has unexpected endpoints {ends}"
    route = os.path.join(work, "route.json")
    with open(route, "w") as f:
        json.dump(direct[0], f, sort_keys=True)
    return route, None


def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("--pred", required=True)
    ap.add_argument("--quick", action="store_true")
    ap.add_argument("--keep", default=None, help="directory to keep the written instances and bundles")
    ap.add_argument("--solve-every", type=int, default=10, help="pred solve every n-th instance")
    args = ap.parse_args()
    pred = os.path.abspath(args.pred)
    if not os.path.exists(pred):
        print(f"CROSS-COMPARE FAILED: no pred binary at {pred}")
        return 2
    work = args.keep or tempfile.mkdtemp(prefix="cross-compare-")
    os.makedirs(work, exist_ok=True)
    try:
        route, err = find_route(pred, work)
        if err:
            print(f"CROSS-COMPARE FAILED (pred): {err}")
            return 2
        insts = shared_instances(args.quick)
        counts = {"instances": 0, "identical_all_three": 0, "scripts_identical": 0,
                  "pred_failures": 0, "mismatch_vs_constructor": 0, "mismatch_vs_adversary": 0,
                  "scripts_disagree": 0, "solved": 0, "solve_mismatch": 0}
        problems = []
        for n, (fam, e, K) in enumerate(insts):
            counts["instances"] += 1
            src = {"data": {"expression": R.to_pred_expr(e), "target": K}, "type": SOURCE, "variant": {}}
            sp = os.path.join(work, f"src-{n:05d}.json")
            bp = os.path.join(work, f"bundle-{n:05d}.json")
            with open(sp, "w") as f:
                json.dump(src, f)
            out, err = run([pred, "reduce", sp, "--via", route, "--json", "-q"])
            if err:
                counts["pred_failures"] += 1
                problems.append(f"[{fam} #{n}] pred reduce failed: {err.splitlines()[0]}")
                continue
            with open(bp, "w") as f:
                f.write(out)
            try:
                bundle = json.loads(out)
                tgt = bundle["target"]
                if tgt.get("type") != "ILP" or tgt.get("variant") != TARGET_VARIANT:
                    raise ValueError(f"target type/variant {tgt.get('type')} {tgt.get('variant')}")
                got = canon_pred(tgt["data"])
            except (ValueError, KeyError, TypeError) as exc:
                counts["pred_failures"] += 1
                problems.append(f"[{fam} #{n}] bundle not understood: {exc}")
                continue
            adv_ilp = R.reduce(e, K)
            adv = canon_pred(adv_ilp)
            con_t = C.reduce(mine_to_c(e), K)
            con = canon_constructor(con_t)
            if adv == con:
                counts["scripts_identical"] += 1
            else:
                counts["scripts_disagree"] += 1
                problems.append(f"[{fam} #{n}] constructor vs adversary: {describe_diff(con, adv)}")
            ok = True
            if got != con:
                counts["mismatch_vs_constructor"] += 1
                problems.append(f"[{fam} #{n}] pred vs constructor: {describe_diff(got, con)}")
                ok = False
            if got != adv:
                counts["mismatch_vs_adversary"] += 1
                problems.append(f"[{fam} #{n}] pred vs adversary: {describe_diff(got, adv)}")
                ok = False
            if ok and adv == con:
                counts["identical_all_three"] += 1
            # end-to-end on a subset: pred solve of the bundle
            if n % args.solve_every == 0 or fam not in ("exhaustive", "random"):
                out, err = run([pred, "solve", bp, "--json", "-q"], timeout=300)
                feasible = bool(R.solve_all(adv_ilp, limit=1))
                if err:
                    counts["pred_failures"] += 1
                    problems.append(f"[{fam} #{n}] pred solve failed: {err.splitlines()[0]}")
                    continue
                counts["solved"] += 1
                res = json.loads(out)
                status = res.get("status")
                if feasible:
                    cfg = res.get("solution")
                    good = (status == "optimal" and isinstance(cfg, list)
                            and len(cfg) == R.count_unions(e) and R.source_eval(e, cfg) == K)
                else:
                    good = status == "infeasible"
                if not good:
                    counts["solve_mismatch"] += 1
                    problems.append(f"[{fam} #{n}] pred solve: status={status} solution={res.get('solution')} "
                                    f"but scripts say feasible={feasible}")
        for p in problems[:30]:
            print("  " + p)
        if len(problems) > 30:
            print(f"  ... {len(problems) - 30} more")
        print("COUNTS: " + json.dumps(counts))
        failed = any(counts[k] for k in ("pred_failures", "mismatch_vs_constructor", "mismatch_vs_adversary",
                                          "scripts_disagree", "solve_mismatch"))
        print("CROSS-COMPARE FAILED" if failed else
              f"CROSS-COMPARE PASSED: {counts['identical_all_three']} identical targets across pred, "
              f"constructor and adversary; {counts['solved']} pred solve round trips")
        return 1 if failed else 0
    finally:
        if not args.keep:
            shutil.rmtree(work, ignore_errors=True)


if __name__ == "__main__":
    sys.exit(main())

"""Independent implementation of IntegerExpressionMembership -> ILP<bool,i64>,
written from proof.typ alone.

Expressions are nested tuples: ('A', v) | ('U', l, r) | ('S', l, r).
Targets use the pred JSON layout of ILP data:
  {"variables": [{"lower_bound":0,"upper_bound":1},...],
   "constraints": [{"comparison":"Eq","rhs":r,"terms":[[i,c],...]}, ...],
   "objective": [], "sense": "Minimize"}
"""
from __future__ import annotations

I64_MAX = (1 << 63) - 1
USIZE_MAX = (1 << 64) - 1


class ConstructionError(Exception):
    pass


class ExtractionError(Exception):
    pass


class SolverBudget(Exception):
    pass


# ---------------------------------------------------------------- source side
def atom(v):
    return ("A", v)


def union(l, r):
    return ("U", l, r)


def ssum(l, r):
    return ("S", l, r)


def preorder(e):
    """List of nodes in preorder (root, left, right)."""
    out = []
    stack = [e]
    while stack:
        n = stack.pop()
        out.append(n)
        if n[0] != "A":
            stack.append(n[2])
            stack.append(n[1])
    return out


def flatten(e):
    """Preorder list of (kind, value, left_index, right_index); indices are
    positions in the list, independent of object identity."""
    out = []

    def go(n):
        t = len(out)
        out.append(None)
        if n[0] == "A":
            out[t] = ("A", n[1], None, None)
        else:
            l = go(n[1])
            r = go(n[2])
            out[t] = (n[0], None, l, r)
        return t

    go(e)
    return out


def count_unions(e):
    return sum(1 for n in preorder(e) if n[0] == "U")


def source_valid(e, K):
    return K > 0 and all(n[1] > 0 for n in preorder(e) if n[0] == "A")


def source_eval(e, config):
    """Mirror of the Rust evaluate(): Some(int) or None; checked i64 add;
    a union consumes a bit only when visited; length must equal U."""
    if len(config) != count_unions(e):
        raise ValueError("wrong length")
    counter = [0]

    def go(n):
        if n[0] == "A":
            return n[1]
        if n[0] == "U":
            idx = counter[0]
            counter[0] += 1
            if idx >= len(config):
                return None
            return go(n[2] if config[idx] else n[1])
        a = go(n[1])
        if a is None:
            return None
        b = go(n[2])
        if b is None:
            return None
        s = a + b
        if s > I64_MAX or s < -I64_MAX - 1:
            return None
        return s

    return go(e)


def source_satisfied(e, K, config):
    return source_eval(e, config) == K


def reachable(e):
    """Independent denotational oracle: the represented set (values > I64_MAX
    are kept as python ints; they can never equal K)."""
    if e[0] == "A":
        return {e[1]}
    L, R = reachable(e[1]), reachable(e[2])
    if e[0] == "U":
        return L | R
    return {a + b for a in L for b in R}


# ---------------------------------------------------------------- reduction
def bitlen(x):
    assert x > 0
    return x.bit_length()


def checked(x):
    if x < 0 or x > USIZE_MAX:
        raise ConstructionError("count overflow")
    return x


def layout(A, S, U, H):
    """Checked sizes (num_vars, num_rows) with a 64-bit usize model."""
    T = checked(checked(2 * A) - 1)
    if S + U != A - 1:
        raise ConstructionError("not a full binary tree")
    nv = checked(T + checked(A * checked(2 * H - 1)))
    nr = checked(1 + checked(2 * S) + U + checked(A * H) + H)
    return nv, nr


def reduce(e, K):
    if not source_valid(e, K):
        raise ConstructionError("invalid source")
    nodes = flatten(e)
    T = len(nodes)
    leaves = [i for i, n in enumerate(nodes) if n[0] == "A"]
    A = len(leaves)
    vals = [nodes[i][1] for i in leaves]
    H = max([bitlen(K)] + [bitlen(v) for v in vals])
    if H > 63:
        raise ConstructionError("H out of range")

    def p(j, b):  # j in 1..A
        return T + (j - 1) * H + b

    def c(j, b):  # 1 <= b < H
        return T + A * H + (j - 1) * (H - 1) + (b - 1)

    nv = T + A * H + A * (H - 1)
    rows = []

    def row(terms, rhs):
        d = {}
        for i, co in terms:
            d[i] = d.get(i, 0) + co
        ts = sorted([i, co] for i, co in d.items() if co != 0)
        rows.append({"comparison": "Eq", "rhs": rhs, "terms": ts})

    row([(0, 1)], 1)
    for t, n in enumerate(nodes):
        if n[0] == "S":
            l, r = n[2], n[3]
            row([(l, 1), (t, -1)], 0)
            row([(r, 1), (t, -1)], 0)
        elif n[0] == "U":
            l, r = n[2], n[3]
            row([(l, 1), (r, 1), (t, -1)], 0)
    for j in range(1, A + 1):
        v = vals[j - 1]
        tj = leaves[j - 1]
        for b in range(H):
            terms = []
            if j > 1:
                terms.append((p(j - 1, b), 1))
            if (v >> b) & 1:
                terms.append((tj, 1))
            if b >= 1:
                terms.append((c(j, b), 1))
            terms.append((p(j, b), -1))
            if b + 1 < H:
                terms.append((c(j, b + 1), -2))
            row(terms, 0)
    for b in range(H):
        row([(p(A, b), 1)], (K >> b) & 1)
    return {
        "variables": [{"lower_bound": 0, "upper_bound": 1} for _ in range(nv)],
        "constraints": rows,
        "objective": [],
        "sense": "Minimize",
    }


# ---------------------------------------------------------------- target side
def target_feasible(ilp, x):
    """Raises on wrong length; returns bool for bounds/rows."""
    if len(x) != len(ilp["variables"]):
        raise ValueError("wrong length")
    for xi, var in zip(x, ilp["variables"]):
        if type(xi) is not int:
            return False
        lo, hi = var["lower_bound"], var["upper_bound"]
        if (lo is not None and xi < lo) or (hi is not None and xi > hi):
            return False
    for r in ilp["constraints"]:
        s = sum(co * x[i] for i, co in r["terms"])
        cmp = r["comparison"]
        if cmp == "Eq" and s != r["rhs"]:
            return False
        if cmp == "Le" and s > r["rhs"]:
            return False
        if cmp == "Ge" and s < r["rhs"]:
            return False
    return True


def solve_all(ilp, limit=None, budget=None):
    """Generic exact enumerator of all binary solutions of an all-equality
    (or Le/Ge) system, by DFS with interval propagation. Independent of the
    construction: it only reads the rows."""
    n = len(ilp["variables"])
    rows = [(r["terms"], r["comparison"], r["rhs"]) for r in ilp["constraints"]]
    occ = [[] for _ in range(n)]
    for k, (ts, _, _) in enumerate(rows):
        for i, _ in ts:
            occ[i].append(k)
    sols = []

    def ok_row(k, x):
        ts, cmp, rhs = rows[k]
        lo = hi = 0
        for i, co in ts:
            if x[i] is None:
                if co > 0:
                    hi += co
                else:
                    lo += co
            else:
                lo += co * x[i]
                hi += co * x[i]
        if cmp == "Eq":
            return lo <= rhs <= hi
        if cmp == "Le":
            return lo <= rhs
        return hi >= rhs

    def propagate(x, trail, touched):
        queue = list(touched)
        while queue:
            k = queue.pop()
            if not ok_row(k, x):
                return False
            ts = rows[k][0]
            for i, _ in ts:
                if x[i] is None:
                    vals = []
                    for val in (0, 1):
                        x[i] = val
                        if ok_row(k, x):
                            vals.append(val)
                        x[i] = None
                    if not vals:
                        return False
                    if len(vals) == 1:
                        x[i] = vals[0]
                        trail.append(i)
                        queue.extend(occ[i])
        return True

    nodes_seen = [0]

    def dfs(x):
        if limit is not None and len(sols) >= limit:
            return
        nodes_seen[0] += 1
        if budget is not None and nodes_seen[0] > budget:
            raise SolverBudget(f"more than {budget} search nodes")
        try:
            i = x.index(None)
        except ValueError:
            if target_feasible(ilp, x):
                sols.append(list(x))
            return
        for val in (0, 1):
            trail = [i]
            x[i] = val
            if propagate(x, trail, occ[i]):
                dfs(x)
            for t in trail:
                x[t] = None

    x = [None] * n
    trail = []
    if propagate(x, trail, range(len(rows))):
        dfs(x)
    return sols


def brute_all(ilp):
    n = len(ilp["variables"])
    out = []
    for m in range(1 << n):
        x = [(m >> i) & 1 for i in range(n)]
        if target_feasible(ilp, x):
            out.append(x)
    return out


# ---------------------------------------------------------------- extraction
def extract(e, K, ilp, x):
    if len(x) != len(ilp["variables"]):
        raise ExtractionError("wrong length")
    if any(type(xi) is not int or xi not in (0, 1) for xi in x):
        raise ExtractionError("non-binary")
    if not target_feasible(ilp, x):
        raise ExtractionError("not a feasible target witness")
    nodes = flatten(e)
    out = []

    def go(t):
        kind, _, l, r = nodes[t]
        if kind == "A":
            return
        if kind == "S":
            go(l)
            go(r)
            return
        if x[r] == 1:
            out.append(True)
            go(r)
        else:
            if x[l] != 1:
                raise ExtractionError("active union with no active child")
            out.append(False)
            go(l)

    go(0)
    U = count_unions(e)
    out += [False] * (U - len(out))
    return out


# ---------------------------------------------------------------- forward lift
def lift(e, K, config):
    """From a satisfying source witness, build the target witness the proof
    describes (activations of visited nodes, running prefix bits, carries)."""
    nodes = flatten(e)
    T = len(nodes)
    leaves = [i for i, n in enumerate(nodes) if n[0] == "A"]
    A = len(leaves)
    vals = [nodes[i][1] for i in leaves]
    H = max([bitlen(K)] + [bitlen(v) for v in vals])
    act = [0] * T
    ctr = [0]

    def go(t):
        act[t] = 1
        kind, _, l, r = nodes[t]
        if kind == "U":
            ch = config[ctr[0]]
            ctr[0] += 1
            go(r if ch else l)
        elif kind == "S":
            go(l)
            go(r)

    go(0)
    pref, carr = [], []
    P = 0
    for j in range(A):
        add = vals[j] * act[leaves[j]]
        cin = 0
        bits, cs = [], []
        for b in range(H):
            s = ((P >> b) & 1) + ((add >> b) & 1) + cin
            bits.append(s & 1)
            cin = s >> 1
            if b + 1 < H:
                cs.append(cin)
        P += add
        pref += bits
        carr += cs
    return act + pref + carr


def to_pred_expr(e):
    if e[0] == "A":
        return {"Atom": e[1]}
    return {("Union" if e[0] == "U" else "Sum"): [to_pred_expr(e[1]), to_pred_expr(e[2])]}


def from_pred_expr(d):
    if "Atom" in d:
        return ("A", d["Atom"])
    if "Union" in d:
        return ("U", from_pred_expr(d["Union"][0]), from_pred_expr(d["Union"][1]))
    return ("S", from_pred_expr(d["Sum"][0]), from_pred_expr(d["Sum"][1]))


def max_magnitude_bits(ilp):
    vals = []
    for r in ilp["constraints"]:
        vals.append(r["rhs"])
        vals += [co for _, co in r["terms"]]
    for v in ilp["variables"]:
        vals += [b for b in (v["lower_bound"], v["upper_bound"]) if b is not None]
    m = max([abs(v) for v in vals] + [0])
    h = 1
    while m >= (1 << h):
        h += 1
    return h

"""Adversary harness for IntegerExpressionMembership -> ILP<bool,i64>.

Built from proof.typ alone; never imports constructor.py.
`run(impl)` checks any implementation exposing reduce(e, K) and
extract(e, K, ilp, x) (the adversary's own by default); mutants.py feeds
deliberately broken ones and expects failures.

Usage: python3 adversary.py [--quick] [--pred PATH]
"""
from __future__ import annotations

import argparse
import itertools
import json
import os
import random
import subprocess
import sys
import tempfile
from collections import Counter

sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import adv_reduction as R  # noqa: E402
from adv_reduction import (  # noqa: E402
    I64_MAX, atom, union, ssum, flatten, count_unions, source_eval, reachable,
    target_feasible, solve_all, brute_all, lift, max_magnitude_bits,
    ConstructionError, ExtractionError, to_pred_expr,
)

SEED = 2026110411
HYP_SEED_1, HYP_SEED_2, HYP_SEED_3, HYP_SEED_4 = 2026110412, 2026110413, 2026110414, 2026110415
HYP_EXAMPLES = 300


class Audit:
    def __init__(self, stop_on_fail=False):
        self.checks = Counter()
        self.fails = Counter()
        self.first = {}
        self.stop = stop_on_fail
        self.instances = Counter()
        self.features = Counter()
        self.fail_sites = set()

    def check(self, section, cond, msg=""):
        self.checks[section] += 1
        if not cond:
            self.fails[section] += 1
            self.fail_sites.add(sys._getframe(1).f_lineno)
            self.first.setdefault(section, msg)
            if self.stop:
                raise AssertionError(f"[{section}] {msg}")
        return cond


# ------------------------------------------------------------ instance families
def shapes(n_leaves):
    """All full binary tree shapes with n leaves (as nested 'X' placeholders)."""
    if n_leaves == 1:
        return ["L"]
    out = []
    for k in range(1, n_leaves):
        for l in shapes(k):
            for r in shapes(n_leaves - k):
                out.append(("X", l, r))
    return out


def fill(shape, ops, vals):
    ops, vals = list(ops), list(vals)

    def go(s):
        if s == "L":
            return atom(vals.pop(0))
        op = ops.pop(0)
        l = go(s[1])
        r = go(s[2])
        return (op, l, r)

    return go(shape)


def all_trees(n_leaves, values):
    for sh in shapes(n_leaves):
        for ops in itertools.product("US", repeat=n_leaves - 1):
            for vals in itertools.product(values, repeat=n_leaves):
                yield fill(sh, ops, vals)


def stats(e):
    nodes = flatten(e)
    A = sum(1 for n in nodes if n[0] == "A")
    U = sum(1 for n in nodes if n[0] == "U")
    S = sum(1 for n in nodes if n[0] == "S")
    return A, S, U, len(nodes)


def H_of(e, K):
    return max([K.bit_length()] + [n[1].bit_length() for n in flatten(e) if n[0] == "A"])


def popsum(e):
    return sum(bin(n[1]).count("1") for n in flatten(e) if n[0] == "A")


def active_signature(e, cfg):
    """The set of visited nodes: configs differing only in unused bits share it."""
    nodes = flatten(e)
    seen = []
    ctr = [0]

    def go(t):
        seen.append(t)
        kind, _, l, r = nodes[t]
        if kind == "U":
            c = cfg[ctr[0]]
            ctr[0] += 1
            go(r if c else l)
        elif kind == "S":
            go(l)
            go(r)

    go(0)
    return tuple(seen), ctr[0]


# ------------------------------------------------------------ per-instance core
def check_instance(a: Audit, impl, e, K, sec="2-equiv", enumerate_target=True,
                   raw_domain=False):
    a.instances[sec] += 1
    A, S, U, T = stats(e)
    H = H_of(e, K)
    try:
        ilp = impl.reduce(e, K)
    except Exception as exc:  # a construction must succeed on every legal instance
        a.check(sec, False, f"reduce raised {exc!r} on {e} K={K}")
        return
    nv = len(ilp["variables"])
    # source side: every config, checked evaluation, vs the denotational oracle
    sat_cfgs = []
    if U <= 12:
        for bits in itertools.product([False, True], repeat=U):
            if source_eval(e, list(bits)) == K:
                sat_cfgs.append(list(bits))
        src_yes = bool(sat_cfgs)
        a.check(sec, src_yes == (K in reachable(e)),
                f"source oracles disagree on {e} K={K}")
    else:
        src_yes = K in reachable(e)
    # forward: every satisfying source witness lifts to a feasible target point
    for cfg in sat_cfgs:
        x = lift(e, K, cfg)
        ok = len(x) == nv and target_feasible(ilp, x)
        a.check("2-forward", ok, f"lift of {cfg} infeasible on {e} K={K}")
    if not enumerate_target:
        return ilp, sat_cfgs
    try:
        sols = solve_all(ilp)
    except R.SolverBudget as exc:
        a.check(sec, False, f"target search exploded ({exc}) on {e} K={K}")
        return ilp, sat_cfgs
    f = a.features
    f[(sec, "yes" if sols else "no")] += 1
    f[(sec, f"H={H}" if H in (1, 62, 63) else "H=other")] += 1
    if U == 0:
        f[(sec, "sum-only")] += 1
    if A == 1:
        f[(sec, "single-atom")] += 1
    if any(v > I64_MAX for v in reachable(e)):
        f[(sec, "overflowing-value-in-tree")] += 1
    if sols and src_yes and K + 0 > 0 and max(reachable(e)) > I64_MAX:
        f[(sec, "yes-with-overflowing-alternative")] += 1
    if any(active_signature(e, c)[1] < U for c in sat_cfgs):
        f[(sec, "witness-with-unused-tail")] += 1
    if not src_yes and K > max(reachable(e)):
        f[(sec, "K-above-all-reachable")] += 1
    if any(any(x[len(flatten(e)) + A * H:]) for x in sols):
        f[(sec, "nonzero-carry")] += 1
    a.check(sec, bool(sols) == src_yes,
            f"feasibility mismatch src={src_yes} tgt={bool(sols)} on {e} K={K}")
    # uniqueness of arithmetic auxiliaries: one target point per active tree
    sigs = {active_signature(e, c)[0] for c in sat_cfgs}
    if U <= 12:
        a.check(sec, len(sols) == len(sigs),
                f"{len(sols)} target points vs {len(sigs)} active trees on {e} K={K}")
    if raw_domain and nv <= 16:
        a.check("8-solver", sorted(map(tuple, brute_all(ilp))) == sorted(map(tuple, sols)),
                f"solver != brute force on {e} K={K}")
    # extraction from every feasible target witness
    for x in sols:
        try:
            cfg = impl.extract(e, K, ilp, x)
        except Exception as exc:
            a.check("3-extract", False, f"extract raised {exc!r} on {e} K={K}")
            continue
        a.check("3-extract", len(cfg) == U and all(type(c) is bool for c in cfg),
                f"extracted length/type wrong {cfg} on {e}")
        ok = len(cfg) == U and source_eval(e, cfg) == K
        a.check("3-extract", ok, f"extracted {cfg} not satisfying on {e} K={K}")
        if ok:
            # unused tail is padded with false, at the end
            _, used = active_signature(e, cfg)
            a.check("3-extract", all(c is False for c in cfg[used:]),
                    f"unused tail not false: {cfg} used={used} on {e}")
            a.check("3-extract", lift(e, K, cfg) == x,
                    f"extraction/lift round trip differs on {e} K={K}")
    # every satisfying config is reached by extraction up to the unused tail
    ext_sigs = set()
    for x in sols:
        try:
            ext_sigs.add(active_signature(e, impl.extract(e, K, ilp, x))[0])
        except Exception:
            pass
    a.check("3-extract", ext_sigs == sigs, f"extraction misses active trees on {e} K={K}")
    # rejection of non-solutions
    if sols:
        x = sols[0]
        for bad in (x[:-1], x + [0]):
            try:
                impl.extract(e, K, ilp, bad)
                a.check("3-reject", False, f"wrong length {len(bad)} accepted")
            except Exception:
                a.check("3-reject", True)
        for i in range(0, nv, max(1, nv // 6)):
            y = list(x)
            y[i] ^= 1
            a.check("3-reject", not target_feasible(ilp, y), f"flip {i} still feasible on {e}")
            try:
                impl.extract(e, K, ilp, y)
                a.check("3-reject", False, f"flipped bit {i} accepted by extract on {e}")
            except Exception:
                a.check("3-reject", True)
        y = list(x)
        y[0] = 2
        try:
            impl.extract(e, K, ilp, y)
            a.check("3-reject", False, "non-binary accepted")
        except Exception:
            a.check("3-reject", True)
    check_sizes(a, ilp, e, K)
    check_structure(a, ilp, e, K)
    return ilp, sat_cfgs


def check_sizes(a, ilp, e, K):
    A, S, U, T = stats(e)
    H = H_of(e, K)
    B = popsum(e)
    nv = len(ilp["variables"])
    nr = len(ilp["constraints"])
    nz = sum(len(r["terms"]) for r in ilp["constraints"])
    a.check("4-size", nv == T + A * (2 * H - 1), f"num_vars {nv} on {e} K={K}")
    a.check("4-size", nr == 1 + 2 * S + U + A * H + H, f"num_constraints {nr} on {e} K={K}")
    a.check("4-size", nz == A * (4 * H - 2) + B + 1 + 4 * S + 3 * U, f"num_nonzeros {nz} on {e} K={K}")
    mb = max_magnitude_bits(ilp)
    a.check("4-size", mb == (1 if H == 1 else 2) and mb <= 2, f"magnitude bits {mb} H={H}")
    a.check("4-size", T == 2 * A - 1 and S + U == A - 1, "tree identities")


def check_structure(a, ilp, e, K):
    nv = len(ilp["variables"])
    a.check("5-struct", ilp["objective"] == [] and ilp["sense"] == "Minimize", "objective")
    a.check("5-struct", all(v == {"lower_bound": 0, "upper_bound": 1} for v in ilp["variables"]),
            "binary bounds")
    used = set()
    for r in ilp["constraints"]:
        idx = [i for i, _ in r["terms"]]
        cos = [c for _, c in r["terms"]]
        a.check("5-struct", r["comparison"] == "Eq", "all rows equalities")
        a.check("5-struct", idx == sorted(set(idx)) and all(0 <= i < nv for i in idx),
                f"terms not sorted/distinct/in range: {r}")
        a.check("5-struct", set(cos) <= {-2, -1, 1} and r["rhs"] in (0, 1), f"coeffs/rhs {r}")
        pos = sum(c for c in cos if c > 0)
        neg = -sum(c for c in cos if c < 0)
        a.check("5-struct", pos <= 3 and neg <= 3 and pos + neg <= 6, f"row magnitude {r}")
        acc, lo, hi = 0, 0, 0
        for c in cos:  # partial accumulation of an arbitrary binary point
            lo, hi = lo + min(c, 0), hi + max(c, 0)
        a.check("5-struct", -3 <= lo and hi <= 3, f"partial accumulation {r}")
        used |= set(idx)
    a.check("5-struct", used == set(range(nv)), "a variable appears in no row")
    # coordinate layout of the proof: root activation is variable 0, pinned to 1
    a.check("5-struct", ilp["constraints"][0] == {"comparison": "Eq", "rhs": 1, "terms": [[0, 1]]},
            "first row is the root pin")


# ------------------------------------------------------------ section 1: symbolic
def section_symbolic(a, impl):
    import sympy as sp
    A, S, U, H, B = sp.symbols("A S U H B", integer=True, positive=True)
    T = 2 * A - 1
    nz_parts = 1 + 4 * S + 3 * U + H * (A - 1) + B + 2 * A * (H - 1) + A * H + H
    a.check("1-symbolic", sp.simplify(nz_parts - (A * (4 * H - 2) + B + 1 + 4 * S + 3 * U)) == 0,
            "nonzero components do not sum to the displayed formula")
    a.check("1-symbolic", sp.simplify(T + A * H + A * (H - 1) - (T + A * (2 * H - 1))) == 0, "vars")
    # single-atom special case
    sub = {A: 1, S: 0, U: 0}
    a.check("1-symbolic", sp.simplify((T + A * (2 * H - 1)).subs(sub) - 2 * H) == 0, "single atom vars")
    a.check("1-symbolic", sp.simplify((1 + 2 * S + U + A * H + H).subs(sub) - (1 + 2 * H)) == 0, "single atom rows")
    a.check("1-symbolic", sp.simplify((A * (4 * H - 2) + B + 1 + 4 * S + 3 * U).subs(sub) - (4 * H - 1 + B)) == 0,
            "single atom nnz")
    # telescoping of the ripple rows at every legal H, with symbolic bits
    for h in range(1, 64):
        p0 = [sp.Symbol(f"pprev_{b}") for b in range(h)]
        p1 = [sp.Symbol(f"pcur_{b}") for b in range(h)]
        vb = [sp.Symbol(f"vbit_{b}") for b in range(h)]
        cs = [0] + [sp.Symbol(f"carry_{b}") for b in range(1, h)] + [0]
        act = sp.Symbol("a")
        total = 0
        for b in range(h):
            row = p0[b] + vb[b] * act + cs[b] - p1[b] - 2 * cs[b + 1]
            total += 2 ** b * row
        P0 = sum(2 ** b * p0[b] for b in range(h))
        P1 = sum(2 ** b * p1[b] for b in range(h))
        V = sum(2 ** b * vb[b] for b in range(h))
        a.check("1-symbolic", sp.expand(total - (P0 + V * act - P1)) == 0, f"telescoping fails at H={h}")
    # tie the algebra to the implementation's emitted rows: for every legal H,
    # build (2^(H-1)) + 1 at K = 2^(H-1) [H=1: 1+1 at K=1], read the stage-2
    # addition rows at the row positions the proof fixes, and check that their
    # 2^b-weighted symbolic sum is P_1 + v_2 a_leaf - P_2 with the proof's indices,
    # and that the formulas evaluated at the instance equal the measured sizes
    for h in range(1, 64):
        v1 = 1 << (h - 1)
        e = ssum(atom(v1), atom(1))
        ilp = impl.reduce(e, v1)
        Ai, Si, Ui, Hi, Bi = 2, 1, 0, h, bin(v1).count("1") + 1
        Ti = 3
        meas = (len(ilp["variables"]), len(ilp["constraints"]),
                sum(len(r["terms"]) for r in ilp["constraints"]))
        forms = [T + A * (2 * H - 1), 1 + 2 * S + U + A * H + H, A * (4 * H - 2) + B + 1 + 4 * S + 3 * U]
        sub = {A: Ai, S: Si, U: Ui, H: Hi, B: Bi}
        a.check("1-symbolic", tuple(int(f.subs(sub)) for f in forms) == meas,
                f"formulas at H={h} give {[f.subs(sub) for f in forms]} vs measured {meas}")
        xs = [sp.Symbol(f"x{i}") for i in range(meas[0])]
        base = 1 + 2 * Si + Ui
        rows = ilp["constraints"]
        if len(rows) < base + 2 * h:
            a.check("1-symbolic", False, f"too few rows at H={h}")
            continue
        total = 0
        for b in range(h):
            r = rows[base + h + b]
            total += 2 ** b * (sum(c * xs[i] for i, c in r["terms"]) - r["rhs"])
        P1 = sum(2 ** b * xs[Ti + b] for b in range(h))
        P2 = sum(2 ** b * xs[Ti + h + b] for b in range(h))
        a.check("1-symbolic", sp.expand(total - (P1 + 1 * xs[2] - P2)) == 0,
                f"emitted stage-2 rows do not telescope at H={h}")
    # local truth table: in + in + cin = r + 2 cout has a unique binary (r, cout)
    for x, y, z in itertools.product((0, 1), repeat=3):
        pairs = [(r, c) for r in (0, 1) for c in (0, 1) if x + y + z == r + 2 * c]
        a.check("1-symbolic", len(pairs) == 1, "full adder not unique")
    # H=1: no carries, 1+1 has no binary result bit
    a.check("1-symbolic", [r for r in (0, 1) if 1 + 1 == r] == [], "H=1 admits 1+1")


# ------------------------------------------------------------ section 2/3: exhaustive
def section_exhaustive(a, impl, quick=False):
    n = 0
    # every full binary tree with at most 5 nodes (<=3 leaves), atoms 1..4, K 1..13
    for leaves in (1, 2, 3):
        for e in all_trees(leaves, range(1, 5)):
            for K in range(1, 14):
                check_instance(a, impl, e, K, raw_domain=True)
                n += 1
    # 7 nodes (4 leaves), atoms 1..3, K 1..10 (sub-sampled when --quick)
    rng = random.Random(SEED)
    trees = list(all_trees(4, range(1, 4)))
    if quick:
        trees = rng.sample(trees, 200)
    for e in trees:
        for K in range(1, 11):
            check_instance(a, impl, e, K)
            n += 1
    # 9 nodes (5 leaves): 300 random per (U,S) cell, atoms 1..6
    for U in range(0, 5):
        S = 4 - U
        cell = 0
        tries = 0
        while cell < (60 if quick else 300) and tries < 100000:
            tries += 1
            sh = rng.choice(shapes(5))
            ops = ["U"] * U + ["S"] * S
            rng.shuffle(ops)
            e = fill(sh, ops, [rng.randint(1, 6) for _ in range(5)])
            reach = sorted(reachable(e))
            K = rng.choice([rng.choice(reach), rng.choice(reach) + 1, max(reach) + 1,
                            max(1, min(reach) - 1), rng.randint(1, 40)])
            check_instance(a, impl, e, K)
            cell += 1
            n += 1
    return n


# ------------------------------------------------------------ hypothesis strategies
def section_hypothesis(a, impl, quick=False):
    from hypothesis import given, settings, seed, strategies as st, HealthCheck

    ex = 60 if quick else HYP_EXAMPLES
    cfg = dict(max_examples=ex, deadline=None, database=None,
               suppress_health_check=list(HealthCheck), derandomize=False)

    def leaf(vals):
        return vals.map(atom)

    def tree(vals, max_leaves=7, union_weight=3):
        return st.recursive(
            leaf(vals),
            lambda ch: st.one_of(
                *([st.tuples(ch, ch).map(lambda p: union(*p))] * union_weight),
                st.tuples(ch, ch).map(lambda p: ssum(*p)),
            ),
            max_leaves=max_leaves,
        )

    # S1: union-heavy nested trees with small atoms; K aimed at reachable
    # boundaries (exact hits, +-1, above the maximum)
    @settings(**cfg)
    @seed(HYP_SEED_1)
    @given(tree(st.integers(1, 9)), st.integers(0, 4), st.data())
    def s1(e, mode, data):
        reach = sorted(reachable(e))
        if mode == 0:
            K = data.draw(st.sampled_from(reach))
        elif mode == 1:
            K = data.draw(st.sampled_from(reach)) + 1
        elif mode == 2:
            K = max(1, data.draw(st.sampled_from(reach)) - 1)
        elif mode == 3:
            K = max(reach) + data.draw(st.integers(1, 64))
        else:
            K = data.draw(st.integers(1, 80))
        check_instance(a, impl, e, K, sec="6-hyp-s1")

    # S2: signed-i64 boundary: atoms near powers of two, i64::MAX, values that
    # overflow in inactive branches; K = MAX or near reachable values
    big = st.one_of(
        st.sampled_from([1, 2, 3, I64_MAX, I64_MAX - 1, 1 << 62, (1 << 62) - 1, (1 << 62) + 1,
                         (1 << 61), (1 << 31) - 1, 1 << 32]),
        st.integers(1, I64_MAX),
        st.integers(0, 62).map(lambda k: max(1, (1 << k) - 1)),
        st.integers(0, 62).map(lambda k: 1 << k),
    )

    @settings(**cfg)
    @seed(HYP_SEED_2)
    @given(tree(big, max_leaves=6, union_weight=2), st.integers(0, 3), st.data())
    def s2(e, mode, data):
        reach = sorted(v for v in reachable(e) if v <= I64_MAX)
        if mode == 0 or not reach:
            K = I64_MAX
        elif mode == 1:
            K = data.draw(st.sampled_from(reach))
        elif mode == 2:
            K = min(I64_MAX, data.draw(st.sampled_from(reach)) + 1)
        else:
            K = data.draw(st.integers(1, I64_MAX))
        check_instance(a, impl, e, K, sec="6-hyp-s2")

    # S3: sum-only trees and single atoms (U = 0), including totals above
    # i64::MAX; K = total, total +- 1, or MAX
    @settings(**cfg)
    @seed(HYP_SEED_3)
    @given(st.lists(big, min_size=1, max_size=6), st.data(), st.integers(0, 3))
    def s3(vals, data, mode):
        e = atom(vals[0])
        for v in vals[1:]:
            e = ssum(e, atom(v)) if data.draw(st.booleans()) else ssum(atom(v), e)
        tot = sum(vals)
        K = [tot, tot + 1, tot - 1, I64_MAX][mode]
        K = min(max(K, 1), I64_MAX)
        check_instance(a, impl, e, K, sec="6-hyp-s3")

    # S4: an overflowing sum (> i64::MAX) placed as one union alternative next to
    # a satisfiable subtree, at random side and depth; K hits the satisfiable side,
    # or forces the overflowing side (NO)
    @settings(**cfg)
    @seed(HYP_SEED_4)
    @given(tree(st.integers(1, 9), max_leaves=4), st.integers(1, I64_MAX), st.integers(1, I64_MAX),
           st.booleans(), st.booleans(), st.integers(0, 2), st.data())
    def s4(e0, x, y, side, outer, mode, data):
        if x + y <= I64_MAX:
            x = I64_MAX - y + 1 + (x % 7) if I64_MAX - y + 1 + (x % 7) <= I64_MAX else I64_MAX
            if x + y <= I64_MAX:
                x, y = I64_MAX, max(y, 1)
        bad = ssum(atom(x), atom(y))
        e = union(bad, e0) if side else union(e0, bad)
        if outer:
            e = ssum(atom(1), e) if side else ssum(e, union(atom(2), atom(3)))
        reach = sorted(v for v in reachable(e) if v <= I64_MAX)
        if mode < 2 and reach:
            K = data.draw(st.sampled_from(reach))
        else:
            K = min(I64_MAX, data.draw(st.integers(1, I64_MAX)))
        check_instance(a, impl, e, K, sec="6-hyp-s4")

    s1()
    s2()
    s3()
    s4()


# ------------------------------------------------------------ section 7: examples
def yes_tree():
    return ssum(ssum(union(atom(1), atom(4)), union(atom(3), atom(6))), union(atom(2), atom(5)))


def section_examples(a, impl):
    sec = "7-examples"
    e = yes_tree()
    A, S, U, T = stats(e)
    ilp = impl.reduce(e, 12)
    a.check(sec, (A, S, U, T, H_of(e, 12), popsum(e)) == (6, 2, 3, 11, 4, 9), "YES params")
    a.check(sec, source_eval(e, [True, True, False]) == 12, "YES source witness")
    x = lift(e, 12, [True, True, False])
    a.check(sec, x[:11] == [1, 1, 1, 0, 1, 1, 0, 1, 1, 1, 0], "YES activations")
    prefix_rows = [(0, 0, 0, 0), (0, 0, 1, 0), (0, 0, 1, 0), (0, 1, 0, 1), (0, 0, 1, 1), (0, 0, 1, 1)]
    carry_rows = [(0, 0, 0), (0, 0, 0), (0, 0, 0), (0, 0, 1), (0, 1, 0), (0, 0, 0)]
    pre = [b for r in prefix_rows for b in r]
    car = [b for r in carry_rows for b in r]
    a.check(sec, x == [1, 1, 1, 0, 1, 1, 0, 1, 1, 1, 0] + pre + car, "YES full 53-vector")
    a.check(sec, len(ilp["variables"]) == 53, "YES 53 vars")
    a.check(sec, len(ilp["constraints"]) == 36, "YES 36 rows")
    a.check(sec, sum(len(r["terms"]) for r in ilp["constraints"]) == 111, "YES 111 nnz")
    a.check(sec, target_feasible(ilp, x), "YES table vector feasible")
    sols = solve_all(ilp)
    a.check(sec, x in sols, "YES table vector among solutions")
    a.check(sec, impl.extract(e, 12, ilp, x) == [True, True, False], "YES extraction")
    Ps = [0, 4, 4, 10, 12, 12]
    for j, r in enumerate(prefix_rows):
        a.check(sec, sum(b << i for i, b in enumerate(r)) == Ps[j], f"P_{j+1}")
    a.check(sec, sum(car) == 2, "exactly two nonzero carries")
    # the two carries the proof names: stage 4 bit 2 -> c_{4,3}; stage 5 bit 1 -> c_{5,2}
    a.check(sec, carry_rows[3][2] == 1 and carry_rows[4][1] == 1, "named carries")
    a.check(sec, len(sols) == 3, "YES has 3 target witnesses (4+6+2, 1+6+5, 4+3+5)")
    # NO example
    ilp7 = impl.reduce(e, 7)
    a.check(sec, sorted(reachable(e)) == [6, 9, 12, 15], "NO reachable set")
    a.check(sec, all(source_eval(e, list(c)) != 7 for c in itertools.product([False, True], repeat=3)),
            "NO source infeasible")
    a.check(sec, H_of(e, 7) == 3, "NO H=3")
    a.check(sec, len(ilp7["variables"]) == 41 and len(ilp7["constraints"]) == 29
            and sum(len(r["terms"]) for r in ilp7["constraints"]) == 87, "NO 41/29/87")
    a.check(sec, [r["rhs"] for r in ilp7["constraints"][-3:]] == [1, 1, 1], "NO final pins (1,1,1)")
    a.check(sec, solve_all(ilp7) == [], "NO target infeasible")
    # the proof: 9,12,15 exceed three bits and cannot acquire a wrapped extension.
    # Checked: forcing the activation pattern of each reachable value gives no solution.
    # Nested/skipped union regression
    e2 = ssum(union(union(atom(1), atom(2)), atom(3)), union(atom(4), atom(5)))
    il2 = impl.reduce(e2, 8)
    s2 = solve_all(il2)
    a.check(sec, len(s2) == 1 and impl.extract(e2, 8, il2, s2[0]) == [True, True, False],
            "nested regression extracts (true,true,false)")
    # K above every reachable value: 1 u 2, K = 8, H = 4
    e3 = union(atom(1), atom(2))
    il3 = impl.reduce(e3, 8)
    a.check(sec, H_of(e3, 8) == 4 and len(il3["variables"]) == 3 + 2 * 7 and solve_all(il3) == [],
            "K above reachable")
    # single atom
    for v, K in ((5, 5), (5, 4), (1, 1), (I64_MAX, I64_MAX), (I64_MAX, 1)):
        il = impl.reduce(atom(v), K)
        H = H_of(atom(v), K)
        sols = solve_all(il)
        a.check(sec, len(il["variables"]) == 2 * H and len(il["constraints"]) == 1 + 2 * H
                and sum(len(r["terms"]) for r in il["constraints"]) == 4 * H - 1 + bin(v).count("1"),
                f"single atom sizes {v},{K}")
        a.check(sec, (len(sols) == 1) == (v == K), f"single atom feasibility {v},{K}")
        if sols:
            a.check(sec, impl.extract(atom(v), K, il, sols[0]) == [], "single atom empty witness")
    # H = 1: 1+1 rejected at K=1; union of ones at K=1 feasible
    il = impl.reduce(ssum(atom(1), atom(1)), 1)
    a.check(sec, solve_all(il) == [] and max_magnitude_bits(il) == 1, "H=1 rejects 1+1")
    il = impl.reduce(union(atom(1), atom(1)), 1)
    a.check(sec, len(solve_all(il)) == 2, "H=1 union of ones feasible (2 witnesses)")
    # H = 63 at i64::MAX, with an inactive overflowing sum under a union
    M = I64_MAX
    for e4, K, want in (
        (ssum(atom(M - 1), atom(1)), M, [[]]),
        (union(ssum(atom(M), atom(1)), atom(M)), M, [[True]]),
        (union(atom(M), ssum(atom(M), atom(1))), M, [[False]]),
        (ssum(atom(M), atom(1)), M, []),
        (union(ssum(atom(M), atom(1)), ssum(atom(1), atom(M))), M, []),
        (ssum(atom(M), atom(1)), 1, []),
    ):
        il = impl.reduce(e4, K)
        sols = solve_all(il)
        a.check(sec, H_of(e4, K) == 63, "H=63")
        a.check(sec, [impl.extract(e4, K, il, s) for s in sols] == want, f"H=63 case {e4}")


def section_claims(a, impl):
    """Prose claims that are not part of a generic instance check."""
    sec = "9-claims"
    M = I64_MAX
    # Revised proof: "H=63 admits atom and K=i64::MAX, and (i64::MAX-1)+1 at
    # that K with no carries. At K=2^62, (2^62-1)+1 gives a 62-long carry chain."
    # (The first proof revision claimed a carry chain for (i64::MAX-1)+1; false.)
    T, A, H = 3, 2, 63
    for e, what in ((ssum(atom(M - 1), atom(1)), "(i64::MAX-1)+1"),
                    (ssum(atom(1), atom(M - 1)), "1+(i64::MAX-1)")):
        il = impl.reduce(e, M)
        sols = solve_all(il)
        a.check("9-claims-prose", H_of(e, M) == 63 and len(sols) == 1
                and impl.extract(e, M, il, sols[0]) == [] and not any(sols[0][T + A * H:]),
                f"{what} at K=i64::MAX: expected one witness with no carries")
    il = impl.reduce(atom(M), M)
    a.check("9-claims-prose", H_of(atom(M), M) == 63 and len(solve_all(il)) == 1,
            "atom i64::MAX at K=i64::MAX feasible at H=63")
    e = ssum(atom((1 << 62) - 1), atom(1))
    il = impl.reduce(e, 1 << 62)
    sols = solve_all(il)
    # carries c_{j,b}: stage 1 (b=1..62) then stage 2 (b=1..62)
    a.check("9-claims-prose", H_of(e, 1 << 62) == 63 and len(sols) == 1
            and sols[0][T + A * H:] == [0] * 62 + [1] * 62,
            "(2^62-1)+1 at K=2^62: expected exactly a 62-long carry chain in stage 2")
    # longest carry chain is 62: stage-2 carries c_{2,1..62}; no c_{2,63} exists
    a.check("9-claims-prose", len(sols[0][T + A * H:]) == 2 * 62 if sols else False,
            "internal carries per stage at H=63 must be 62")
    # a genuine 62-long carry chain at H=63: (2^62-1) + 1 + (2^62-1) = i64::MAX
    e = ssum(ssum(atom((1 << 62) - 1), atom(1)), atom((1 << 62) - 1))
    il = impl.reduce(e, M)
    sols = solve_all(il)
    a.check(sec, len(sols) == 1 and impl.extract(e, M, il, sols[0]) == [], "H=63 carry chain feasible")
    if sols:
        c2 = sols[0][5 + 3 * 63 + 62: 5 + 3 * 63 + 2 * 62]
        a.check(sec, c2 == [1] * 62, "stage 2 carries all ones (62-long chain)")
    # at K = i64::MAX (all ones) the last active stage can never carry
    # inactive overflowing alternative: activations zero its leaves
    e = union(ssum(atom(M), atom(1)), atom(M))
    il = impl.reduce(e, M)
    (x,) = solve_all(il)
    a.check(sec, x[:5] == [1, 0, 0, 0, 1], "inactive overflowing sum has zero activations")
    # missing terminal carry: a free final carry would admit modular wrap (15 = 7 mod 8)
    e = yes_tree()
    il = impl.reduce(e, 7)
    a.check(sec, solve_all(il) == [] and (15 % 8) == 7, "wrap would be 15 = 7 mod 8")
    # checked layout arithmetic at a 64-bit usize: last valid vs first invalid A (H=63)
    H = 63
    per = 2 * H - 1
    # largest A with 2A-1 + A*per <= USIZE_MAX
    Amax = (R.USIZE_MAX + 1) // (2 + per)
    ok = True
    try:
        R.layout(Amax, Amax - 1, 0, H)
    except ConstructionError:
        ok = False
    a.check(sec, ok, "last valid layout rejected")
    try:
        R.layout(Amax + 1, Amax, 0, H)
        a.check(sec, False, "first invalid layout accepted")
    except ConstructionError:
        a.check(sec, True)
    # H endpoints: H from bit lengths; 2^62 -> 63 bits, 2^62-1 -> 62, MAX -> 63
    a.check(sec, H_of(atom(1 << 62), 1) == 63 and H_of(atom((1 << 62) - 1), 1) == 62
            and H_of(atom(1), M) == 63 and H_of(atom(1), 1) == 1, "H endpoints")
    # rejected neighbours: 0 and 2^63 are not legal source numbers
    for v, K in ((0, 1), (1, 0), (-1, 1), (1 << 63, 1), (1, 1 << 63)):
        try:
            impl.reduce(atom(v), K)
            a.check(sec, (1 <= v <= M and 1 <= K <= M), f"illegal input {v},{K} accepted")
        except Exception:
            a.check(sec, True)
    # i64 wrapping would admit M + M + 3 = 1 (mod 2^64); checked/exact arithmetic must not
    e = ssum(ssum(atom(M), atom(M)), atom(3))
    a.check(sec, source_eval(e, []) != 1 and solve_all(impl.reduce(e, 1)) == [],
            "wrapped sum M+M+3 accepted as 1")
    # extraction never reserves bits for skipped unions: static-index decoding differs
    e2 = ssum(union(union(atom(1), atom(2)), atom(3)), union(atom(4), atom(5)))
    a.check(sec, source_eval(e2, [True, False, True]) == 7 and source_eval(e2, [True, True, False]) == 8,
            "static preorder indices would decode the regression incorrectly")


# ------------------------------------------------------------ pred calibration
def section_pred(a, pred):
    """Calibrate the adversary's source evaluator and target checker against
    the Rust models through `pred evaluate`."""
    sec = "10-pred-calib"
    rng = random.Random(SEED + 7)
    with tempfile.TemporaryDirectory() as d:
        def ev(obj, cfg):
            p = os.path.join(d, "x.json")
            with open(p, "w") as f:
                json.dump(obj, f)
            r = subprocess.run([pred, "evaluate", p, "--config", json.dumps(cfg), "--json", "-q"],
                               capture_output=True, text=True)
            if r.returncode != 0:
                return None
            return json.loads(r.stdout)["result"]
        M = I64_MAX
        cases = [(yes_tree(), 12), (yes_tree(), 7),
                 (ssum(union(union(atom(1), atom(2)), atom(3)), union(atom(4), atom(5))), 8),
                 (union(ssum(atom(M), atom(1)), atom(M)), M),
                 (union(atom(M), ssum(atom(M), atom(1))), M), (ssum(atom(M), atom(1)), M)]
        for _ in range(25):
            sh = rng.choice(shapes(rng.randint(1, 5)))
            n_ops = str(sh).count("X")
            e = fill(sh, [rng.choice("US") for _ in range(n_ops)],
                     [rng.choice([1, 2, 3, 7, M, M - 1, 1 << 62]) for _ in range(n_ops + 1)])
            cases.append((e, rng.choice([1, 3, 5, M, rng.randint(1, M)])))
        for e, K in cases:
            src = {"data": {"expression": to_pred_expr(e), "target": K},
                   "type": "IntegerExpressionMembership", "variant": {}}
            U = count_unions(e)
            for bits in itertools.product([False, True], repeat=U):
                mine = source_eval(e, list(bits)) == K
                got = ev(src, list(bits))
                a.check(sec, got == f"Or({str(mine).lower()})", f"pred {got} vs mine {mine} on {e} {bits}")
            got = ev(src, [False] * (U + 1))
            a.check(sec, got is None, "pred accepted wrong-length source config")
            ilp = R.reduce(e, K)
            tgt = {"data": ilp, "type": "ILP",
                   "variant": {"bounds": "general", "coefficient": "i64", "variable": "bool"}}
            sols = solve_all(ilp)
            nv = len(ilp["variables"])
            pts = list(sols) + [[rng.randint(0, 1) for _ in range(nv)] for _ in range(2)]
            if sols:
                y = list(sols[0]); y[-1] ^= 1
                pts.append(y)
            for x in pts:
                mine = target_feasible(ilp, x)
                got = ev(tgt, x)
                a.check(sec, got == ("Min(0)" if mine else "Min(None)"), f"pred {got} vs mine {mine}")


# ------------------------------------------------------------ driver
def run(impl=R, quick=False, pred=None, stop_on_fail=False, sections=None):
    a = Audit(stop_on_fail)
    todo = sections or ["symbolic", "exhaustive", "hypothesis", "examples", "claims", "pred"]
    for name in todo:
        try:
            if name == "symbolic":
                section_symbolic(a, impl)
            elif name == "exhaustive":
                section_exhaustive(a, impl, quick)
            elif name == "hypothesis":
                section_hypothesis(a, impl, quick)
            elif name == "examples":
                section_examples(a, impl)
            elif name == "claims":
                section_claims(a, impl)
            elif name == "pred" and pred:
                section_pred(a, pred)
        except Exception as exc:  # a crash inside a section is a failure of that section
            if stop_on_fail:
                raise
            a.check(f"crash-{name}", False, f"{type(exc).__name__}: {exc}")
    return a


def report(a):
    total_c = sum(a.checks.values())
    total_f = sum(a.fails.values())
    for s in sorted(set(a.checks) | set(a.fails)):
        line = f"{s:18s} {a.checks[s]:8d} checks {a.fails[s]:6d} failures"
        if a.instances.get(s):
            line += f"   ({a.instances[s]} instances)"
        print(line)
        if a.fails[s]:
            print(f"    first failure: {a.first[s]}")
    print(f"instances: {dict(a.instances)}")
    print("feature coverage (instances):")
    for (s, k), v in sorted(a.features.items()):
        print(f"    {s:12s} {k:34s} {v}")
    print(f"TOTAL: {total_c} checks, {total_f} failures")
    return total_f


if __name__ == "__main__":
    ap = argparse.ArgumentParser()
    ap.add_argument("--quick", action="store_true")
    ap.add_argument("--pred", default=None)
    args = ap.parse_args()
    a = run(quick=args.quick, pred=args.pred)
    sys.exit(1 if report(a) else 0)